\begin{tabbing}
$\forall$\=$a$:Id, $T$:Top, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, ${\it init}$:$x$:Id fp$\rightarrow$ Top, $a_{1}$:Id, $T_{1}$:Top, $d_{1}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]$P_{1}$:Top.
\-\\[0ex]${\it ds}$ $\parallel$ $d_{1}$
\\[0ex]$\Rightarrow$ $\neg$$a$ $=$ $a_{1}$
\\[0ex]$\Rightarrow$ (\=(\=with ds: $d_{1}$\+\+
\\[0ex]action $a_{1}$:$T_{1}$
\\[0ex]precondition $a_{1}$(v) is
\\[0ex]$P_{1}$ s v)
\-\\[0ex]$\Vert\!+$ with ds: ${\it ds}$ init: ${\it init}$action $a$:$T$ precondition $a$(v) is $P$)
\-
\end{tabbing}